nLab inductive-recursive type

Idea

In type theory, induction-recursion is a principle for mutually defining types of the form

$$A \; \mathrm{type} \qquad a:A \vdash B(a) \; \mathrm{type}$$

where $A$ is defined as an inductive type and $B$ is defined by recursion on $A$. Crucially, the definition of $A$ may use $B$. Without this last requirement, we could first define $A$ and then separately $B$.

In type theory, higher induction-reduction is the principle that one could also have identity constructors and identity section constructors in addition to the element and section constructors.

Example

A Tarski universe is an example of an inductive-recursive definition, where a type $U$ is defined inductively together with a type family $a:U \vdash T(a) \; \mathrm{type}$. The constructors for $U$ may depend negatively on $T$ applied to elements of $U$. This is the case if $U$, for example, is closed under dependent product types, where it has constructors of

• a dependent type $\Pi(a, b):U$ for each $a:U$ and $b:T(a) \to U$,
• a function $E_\Pi(a, b):\left(\prod_{x:T(a)} T(b(x))\right) \to T(\Pi(a, b))$ for each $a:U$ and $b:T(a) \to U$.

If the Tarski universe is strictly closed under dependent product types, then the last condition is replaced by

• a judgmental equality $T(\Pi(a, b)) \equiv \prod_{x:T(a)} T(b(x))$ for each $a:U$ and $b:T(a) \to U$.

Here, the type family $T$ is defined recursively. Sometimes, however, one might not want to give $T(u)$ completely as soon as $u:U$ is introduced, but instead define $T$ inductively as well. This is the principle of induction-induction.

Related concepts

• inductive-inductive type

• algebraically compact category

References

History of inductive types

Historical references on the definition of inductive types.

Precursors

A first type theoretic formulation of general inductive definitions:

• Per Martin-Löf, Hauptsatz for the Intuitionistic Theory of Iterated Inductive Definitions, Studies in Logic and the Foundations of Mathematics 63 (1971) 179-216 $[$doi:10.1016/S0049-237X(08)70847-4$]$

The induction principle for identity types (also known as “path induction” or the “J-rule”) is first stated in:

• Per Martin-Löf, §1.7 and p. 94 of: An intuitionistic theory of types: predicative part, in: H. E. Rose, J. C. Shepherdson (eds.), Logic Colloquium ‘73, Proceedings of the Logic Colloquium, Studies in Logic and the Foundations of Mathematics 80 (1975) 73-118 (doi:10.1016/S0049-237X(08)71945-1, CiteSeer)

and in the modern form of inference rules in:

• Bengt Nordström, Kent Petersson, Jan M. Smith, §8.1 of: Programming in Martin-Löf’s Type Theory, Oxford University Press (1990) $[$webpage, pdf, pdf$]$

The special case of inductive types now known as $\mathcal{W}$-types is first formulated in:

• Per Martin-Löf, pp. 171 of: Constructive Mathematics and Computer Programming, in: Proceedings of the Sixth International Congress of Logic, Methodology and Philosophy of Science (1979), Studies in Logic and the Foundations of Mathematics 104 (1982) 153-175 $[$doi:10.1016/S0049-237X(09)70189-2, ISBN:978-0-444-85423-0$]$

• Per Martin-Löf (notes by Giovanni Sambin), Intuitionistic type theory, Lecture notes Padua 1984, Bibliopolis, Napoli (1984) $[$pdf, pdf$]$

Early proposals for a general formal definition of inductive types:

• Robert L. Constable, N. Paul Francis Mendler, Recursive definitions in type theory, in Logic of Programs 1985, Lecture Notes in Computer Science 193 Springer (1985) $[$doi:10.1007/3-540-15648-8_5$]$

• Paul Francis Mendler, Inductive Definition in Type Theory, Cornell (1987) $[$hdl:1813/6710$]$

• Roland Backhouse, On the Meaning and Construction of the Rules of Martin-Löf’s Theory of Types, in: Workshop on General Logic, ECS-LFCS-88-52 (1988) $[$pdf, pdf$]$

Modern definition

The modern notion of inductive types and inductive families in intensional type theory is independently due to

• Peter Dybjer, Inductive sets and families in Martin-Löf’s type theory and their set-theoretic semantics, Logical frameworks (1991) 280-306 $[$doi:10.1017/CBO9780511569807.012, pdf$]$

• Peter Dybjer, Inductive families, Formal Aspects of Computing 6 (1994) 440–465 $[$doi:10.1007/BF01211308, doi:10.1007/BF01211308, pdf$]$

and due to

• Thierry Coquand, Christine Paulin, Inductively defined types, COLOG-88 Lecture Notes in Computer Science 417, Springer (1990) 50-66 $[$doi:10.1007/3-540-52335-9_47$]$

which became the basis of the calculus of inductive constructions used in the Coq-proof assistant:

• Frank Pfenning, Christine Paulin-Mohring, Inductively defined types in the Calculus of Constructions, in: Mathematical Foundations of Programming Semantics MFPS 1989, Lecture Notes in Computer Science 442, Springer (1990) $[$doi:10.1007/BFb0040259$]$

• Christine Paulin-Mohring, Inductive definitions in the system Coq – Rules and Properties, in: Typed Lambda Calculi and Applications TLCA 1993, Lecture Notes in Computer Science 664 Springer (1993) $[$doi:10.1007/BFb0037116$]$

reviewed in

• Zhaohui Luo, §9.2.2 in: Computation and Reasoning – A Type Theory for Computer Science, Clarendon Press (1994) $[$ISBN:9780198538356, pdf$]$

• Christine Paulin-Mohring, §2.2. in: Introduction to the Calculus of Inductive Constructions, contribution to: Vienna Summer of Logic (2014) $[$hal:01094195, pdf, pdf slides$]$

with streamlined exposition in:

• Univalent Foundations Project, §5.6 of: Homotopy Type Theory – Univalent Foundations of Mathematics (2013) $[$web, pdf$]$

The generalization to inductive-recursive types is due to

• Peter Dybjer, A general formulation of simultaneous inductive-recursive definitions in type theory, The Journal of Symbolic Logic 65 2 (2000) 525-549 $[$doi:10.2307/2586554, pdf$]$

• Peter Dybjer, Anton Setzer, Indexed induction-recursion, in Proof Theory in Computer Science PTCS 2001. Lecture Notes in Computer Science2183 Springer (2001) $[$doi:10.1007/3-540-45504-3_7, pdf$]$

See also:

• Peter Dybjer, Inductive and inductive-recursive definitions in type theory (link list)

Further development

(…)